$\forall$$A$:Type, $d_{1}$, $d_{2}$:EqDecider($A$), $f$:$a$:$A$ fp$\rightarrow$ Type, $x$:$A$, $z$:Type. $f$($x$)?$z$ $\subseteq$r $f$($x$)?$z$